Nuprl Lemma : l_member-set
11,40
postcript
pdf
T
:Type,
L
:(
T
List),
x
:
T
. (
x
L
)
(
x
L
)
latex
Definitions
x
.
t
(
x
)
,
P
Q
,
{
T
}
,
x
:
A
.
B
(
x
)
,
t
T
,
x
L
.
P
(
x
)
,
(
x
l
)
Lemmas
l
member
wf
,
l
member
set
origin
T:Type, L:(T List), x:T. (x 
L) 
(x L) T:Type, L:(T List), x:T. (x L) (x L) 
x. t(x) Qx:A. B(x) TxL. P(x) l)